COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	declare INDCONST S0 ε situation
C00005 ENDMK
C⊗;
declare INDCONST S0 ε situation;
declare INDCONST Robot Outside Table Box1 Box2 Door ε tower;
declare PREDCONST key(tower) [pre];
declare PREDCONST red(tower)[pre];
declare PREDCONST theseblocks(tower);
extension theseblocks {Box1 Box2 Door Outside Robot Table};

axiom movable:
	∀t1 t2 s.(movable(t1,t2,s) ≡
(t1 = Robot ∧ (t2 = Box1 ∨ t2 = Box2 ∨ t2 = Door ∨ t2 = Table ∨ t2 = Outside)
	∧ (¬(t2 = Outside) ∨ ∃t.(key t ∧ on(t,Door,s))))
∨ (t2 = Robot ∧ ∀t4.¬on(t4,Robot,s) ∧
	∃t3.(on(Robot,t3,s) ∧ on(t1,t3,s)))
∨ (on(t1,Robot,s) ∧ on(Robot,t2,s)))
;;

axiom initial:
	∃t1 t2.(key t1 ∧ (t2 = Box1 ∨ t2 = Box2) ∧ on(t1,t2,S0)
		∧ ∀t3.(on(t3,t2,S0) ⊃ key t3 ∨ t3 = Robot))

	∃t1.(red t1 ∧ on(t1,Door,S0))

	∀t1.(on(t1,Door,S0) ⊃ red t1 ∨ t1 = Robot)

	∀t.(on(t,Table,S0) ⊃ t = Robot)

	∀t1 t2.(on(t1,Robot,S0) ∧ on(t2,Robot,S0) ⊃ t1 = t2)

	¬on(Robot,Outside,S0)
;;

declare OPCONST pickup(situation) = situation [pre];

axiom pickup:
	∀t s.(on(Robot,t,s) ∧ ∀t1.(on(t1,t,s) ⊃ t = Robot) ⊃ pickup s = s)
	∀t s.(on(Robot,t,s) ∧ ∃t1.(on(t1,t,s) ∧ ¬(t1 = Robot))
		⊃ ∃t1.(¬(t1 = Robot) ∧ pickup s = move(t1,Robot,s)))
;;

declare OPCONST drop(situation) = situation [pre];

axiom drop:
	∀t s.(∀t1.¬on(t1,Robot,s) ⊃ drop s = s)
	∀t s t1.(on(Robot,t,s) ∧ on(t1,Robot,s) ⊃ drop s = move(t1,t,s))
;;

declare OPCONST go(tower, situation) = situation;

axiom go:
	∀t s.(go(t,s) = move(Robot,t,s))
;;